Symbolic model checking is commonly used to check, or verify, an integrated circuit design before the integrated circuit design is implemented in a semiconductor device. In symbolic model checking, a model of an environment in which the semiconductor device is intended to function is constructed. FIG. 1 illustrates, in block diagram form, a prior art model checking wrapper 10 that includes an environment module 12 that is bi-directionally coupled to a design under analysis (DUA) module 14. The environment model is separate from the DUA, and includes environmental constraints that control the input signals provided to the integrated circuit design during model checking.
In some digital circuit designs, it may be possible to simply provide every combination of input bits to the DUA model and observe the outputs. However, many circuits are designed to work correctly only under certain specific environmental constraints, or assumptions. The environmental assumptions are used to simulate, as closely as possible, the actual input signals which would be received by the integrated circuit in its intended application. However, constructing the environment model is difficult, time-consuming and potentially error-prone for large complex circuits and systems. Also, there exists no clear methodology for ensuring that the environment model is a true abstraction of the actual environment in which the integrated circuit is designed to operate.